T:Type, R:(TT), P:(T).
(x, y:T. Dec(R(x,y)))
 (x:T. Dec(P(x)))
 (y:T. L:T List. (x:T. (R(x,y))  (x  L)))
 WellFnd{i}(T;x,y.R(x,y))
 (z:T. (P(z))  (y:T. (P(y) & (R^*)(y,z) & (x:T. (R^+(x,y))  ((P(x))))))) 

latex

Definitions	t  T, Type, x:AB(x), , x:A  B(x), Void, False, x.A(x), {T}, x. t(x), WellFnd{i}(A;x,y.R(x;y)), x(s), Dec(P), type List, (x  l), f(a), A, R^+, P  Q, x:A. B(x), R^*, P & Q, x:A. B(x), left + right, P  Q, x f y, s = t, a < b, A c B, rel_exp(T;R;n), , P  Q, s ~ t, SQType(T)
Lemmas	rel-star-iff-rel-plus-or, nat plus wf, rel exp wf, nat plus inc, rel rel star, rel-plus-rel-star, rel star weakening, rel star transitivity, rel plus implies, decidable wellfound-bounded-exists, rel star wf, rel plus wf, not wf